@Misc{jml-models-api,
	author = {Gary T. Leavens and Clyde Ruby and Albert L. Baker},
	title  ={org.jmlspecs.models Package Documentation},
	year = {2008},
	note = {http://\-www.eecs.ucf.edu/\~{}leavens/\-JML-release/\-javadocs/\-org/\-jmlspecs/\-models/\-package-summary.html}
}

@Misc{jml-dbc,
	author = {Gary T. Leavens and Y. Cheon},
	title  ={Design by Contract with JML},
	year = {2006},
	note = {http://\-www.\-jmlspecs.\-org}
}

@INPROCEEDINGS{spec-sharp-reference,
  author    = {Mike Barnett, K. Rustan M. Leino, and Wolfram Schulte},
  title     = {The Spec\# programming system: An overview},
  booktitle = {CASSIS 2004},
  year      = {2004},
  pages     = {49-69}
}


@inproceedings{massoniEtAl2008,
  author    = {Tiago Massoni and Rohit Gheyi and Paulo Borba},
  title = {Formal Model-Driven Program Refactoring},
  booktitle     = {11th Fundamental Approaches to Software Engineering (ETAPS)},
  year = {2008},
  pages = {362-376},
  editor    = {Jos{\'e} Luiz Fiadeiro and Paola Inverardi},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {4961},
  year      = {2008},
  isbn      = {978-3-540-78742-6}
}


@INPROCEEDINGS{setra06,
  title = {An Approach to Invariant-based Program Refactoring},
  author    = {Tiago L. Massoni and R. Gheyi and P. Borba},
  booktitle = {Software Evolution through Transformations: Embracing the Change},
  year = {2006},
  pages = {91-101},
  address = {Natal, Brazil}
}

@BOOK{refact-book,
  title = {{Refactoring---Improving the Design of Existing Code}},
  publisher = {Addison Wesley},
  year = {1999},
  author = {Martin Fowler},
  owner = {prof04},
  timestamp = {2007.11.30}
}

@BOOK{DBC-example-book,
  author = {Richard Mitchell and Jim McKim},
  title = {{Design by Contract by Example}},
  publisher = {Addison Wesley},
  year = {2002}
}

@BOOK{eiffel-book,
  author = {Bertrand Meyerr},
	title = {{Eiffel: The Language}},
  publisher = {Prentice Hall},
  year = {1991}
}

@BOOK{latex-book,
  title = {{LaTeX : A Documentation Preparation System}},
  publisher = {Addison-Wesley},
  year = {1994},
  author = {Leslie Lamport}
}

@BOOK{alloy-book-published,
  title = {Software Abstractions: Logic, Language and Analysis},
  publisher = {MIT Press},
  year = {2006},
  author = {D. Jackson},
  owner = {prof04},
  timestamp = {2007.11.30}
}


@ARTICLE{jml-paper,
  author = {Lilian Burdy and Yoonsik Cheon and David Cok and Michael D. Ernst
	and Joe Kiniry and Gary T. Leavens and K. Rustan M. Leino and Erik
	Poll},
  title = {{An Overview of {JML} Tools and Applications}},
  journal = {Software Tools for Technology Transfer},
  year = {2005},
  owner = {prof04},
  timestamp = {2007.11.30}
}

@ARTICLE{dbc-meyer,
  author = {Bertrand Meyer},
  title = {{Design by Contract}},
  journal = {Advances in Object-Oriented Software Engineering},
  year = {1991},
  pages = {1--50}
}

@BOOK{refact-workbook,
  title = {{Refactoring Workbook}},
  publisher = {Addison-Wesley},
  year = {2003},
  author = {William C. Wake}
}

@TECHREPORT{jml-reference,
  author = {{Gary T. Leavens and Erik Poll and Curtis Clifton and Yoonsik Cheon and Clyde Ruby and David Cok and Peter M$\ddot{u}$ller and Joseph Kiniry and Patrice Chalin and Daniel Zimmerman and Werner Dietl}},
  title = {{JML Reference Manual}},
  year = {{2008}},
  month = {May},
}


@INPROCEEDINGS{gpem09,
title={Identifying Architectural Bad Smells},
author={Garcia, J. and Popescu, D. and Edwards, G. and Medvidovic, N.},
booktitle={Software Maintenance and Reengineering, 2009. CSMR '09. 13th European Conference on},
year={2009},
month={March},
volume={},
number={},
pages={255-258},
abstract={Certain design fragments in software architectures can have a negative impact on system maintainability. In this paper, we introduce the concept of architectural "bad smells," which are frequently recurring software designs that can have non-obvious and significant detrimental effects on system lifecycle properties. We define architectural smells and differentiate them from related concepts, such as architectural antipatterns and code smells. We also describe four representative architectural smells we encountered in the context of reverse-engineering eighteen grid technologies and refactoring one large industrial system.},
keywords={grid computing, reverse engineering, software architecture, software maintenancearchitectural bad smell identification, design fragments, grid technologies, industrial system refactoring, reverse engineering, software architectures, system lifecycle properties, system maintainability},
doi={10.1109/CSMR.2009.59},
ISSN={1534-5351}, }

---------------------------------------------------------------------------------------------

 @INPROCEEDINGS{mvl03,
title={A taxonomy and an initial empirical study of bad smells in code},
author={M\"{a}ntyl\"{a}, M. and Vanhanen, J. and Lassenius, C.},
booktitle={International Conference on Software Maintenance },
year={2003},
month={Sept.},
volume={},
number={},
pages={ 381-384},
abstract={ This paper presents research in progress, as well as tentative findings related to the empirical study of so called bad code smells. We present a taxonomy that categorizes similar bad smells. We believe that taxonomy makes the smells more understandable and recognizes the relationships between smells. Additionally, we present our initial findings from an empirical study of the use of the smells for evaluating code quality in a small Finnish software product company. Our findings indicate that the taxonomy for the smells could help explain the identified correlations between the subjective evaluations of the existence of the smells.},
keywords={ object-oriented programming, program compilers, software maintenance, software performance evaluation, software quality bad code smells, code quality, correlations, empirical study, object-oriented context, software quality, taxonomy},
doi={10.1109/ICSM.2003.1235447},
ISSN={1063-6773 }, }


@INPROCEEDINGS{tcc08,
title={JDeodorant: Identification and Removal of Type-Checking Bad Smells},
author={Tsantalis, N. and Chaikalis, T. and Chatzigeorgiou, A.},
booktitle={12th European Conference on Software Maintenance and Reengineering},
year={2008},
month={April},
volume={},
number={},
pages={329-331},
abstract={In this demonstration, we present an Eclipse plug-in that automatically identifies type-checking bad smells in Java source code, and resolves them by applying the "replace conditional with polymorphism" or "replace type code with state/strategy " refactorings. To the best of our knowledge there is a lack of tools that identify type-checking bad smells. Moreover, none of the state-of-the-art IDEs support the refactorings that resolve such kind of bad smells.},
keywords={Java, polymorphism, software maintenance, software quality, source codingEclipse plug-in, JDeodorant, Java source code, polymorphism, refactorings, software maintenance, software quality, type-checking bad smells},
doi={10.1109/CSMR.2008.4493342},
ISSN={1534-5351}, }



@InProceedings{piveta-sbes05,
author = {E. K. Piveta and others},
title = {{Bad Smells em Sistemas Orientados a Aspectos}},
booktitle = {XIX Simp\'{o}sio Brasileiro de Engenharia de Software},
pages = {184---199},
year = {2005}
}


@INPROCEEDINGS{sm07,
title={Defining and Detecting Bad Smells of Aspect-Oriented Software},
author={Srivisut, K. and Muenchaisri, P.},
booktitle={31st Annual International Computer Software and Applications Conference},
year={2007},
month={July},
volume={1},
number={},
pages={65-70},
abstract={Bad smells are software patterns that are generally associated with bad design and bad programming. They can be removed by using the refactoring technique which improves the quality of software. Aspect-oriented (AO) software development, which involves new notions and the different ways of thinking for developing software and solving the crosscutting problem, possibly introduces different kinds of design flaws. Defining bad smells hidden in AO software in order to point out bad design and bad programming is then necessary. This paper proposes the definition of new AO bad smells. Moreover, appropriate existing AO refactoring methods for eliminating each bad smell are presented. The proposed bad smells are validated. The results show that after removing the bad smells by using appropriate refactoring methods, the software quality is increased.},
keywords={object-oriented programming, program verification, software maintenance, software qualityaspect-oriented software, software pattern, software quality, software refactoring},
doi={10.1109/COMPSAC.2007.103},
ISSN={0730-3157}, }


@INPROCEEDINGS{4539545,
title={Contract-Based Verification for Aspect-Oriented Refactoring},
author={Ubayashi, N. and Jinji Piao and Shinotsuka, S. and Tamai, T.},
booktitle={1st International Conference on Software Testing, Verification, and Validation},
year={2008},
month={April},
volume={},
number={},
pages={180-189},
abstract={Refactoring is a method for improving a program's structure without changing its external behavior. Refactoring is a promising approach to assist reliable and safe software evolution. However, in aspect-oriented programming (AOP), it is not necessarily easy for a programmer to understand the overall behavior of a woven program because the weaving modifies the behavior. Unexpected bugs can be embedded in a program if the programmer does not modify the program carefully. In order to deal with this problem, we propose the notion of RbC (refactoring by contract), a technique to verify refactoring based on contracts. Contracts in RbC consist of preconditions, postconditions, and invariants. A precondition states under which conditions refactoring can be applied. A postcondition states what condition should be verified after refactoring has been accomplished, and an invariant states what conditions refactoring should preserve. After introducing RbC, we check whether refactoring preserves behavior and whether it actually improves internal structure. A contract is described in COW (contract writing language), a language for describing a predicate based on first-order logic. COW provides a set of primitive predicates that represent program structure and behavior. Adopting our approach, software evolution in AOP becomes reliable and safe.},
keywords={formal logic, formal verification, object-oriented programming, software reliabilityaspect-oriented refactoring, contract writing language, contract-based verification, first-order logic, primitive predicates, program behavior, program structure, refactoring by contract, software evolution reliability},
doi={10.1109/ICST.2008.36},
ISSN={}, }

@article{DarvasMueller08,
 author = {Darvas, \'A. and M\"uller, P.},
 title = {Faithful mapping of model classes to mathematical structures},
 journal = {IET Software},
 month = {December},
 year = {2008},
 volume = {2},
 number = {6},
 pages = {477--499}
}

@inproceedings{cwb07-models,
 author    = {Alexandre L. Correa and
               Cl{\'a}udia Werner and
               M{\'a}rcio de Oliveira Barros},
  title     = {An Empirical Study of the Impact of OCL Smells and Refactorings
               on the Understandability of OCL Specifications},
  booktitle = {10th Model Driven Engineering Languages and Systems},
  year      = {2007},
  pages     = {76-90},
 }

@inproceedings{ct06-sac,
 author = {Cabot, J. and Teniente, E.},
 title = {Transforming OCL constraints: a context change approach},
 booktitle = {SAC '06: Proceedings of the 2006 ACM symposium on Applied computing},
 year = {2006},
 isbn = {1-59593-108-2},
 pages = {1196--1201},
 location = {Dijon, France},
 doi = {http://doi.acm.org/10.1145/1141277.1141562},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@inproceedings{rgpm06-sac,
 author = {Reynoso, Luis and Genero, Marcela and Piattini, Mario and Manso, Esperanza},
 title = {Does object coupling really affect the understanding and modifying of OCL expressions?},
 booktitle = {SAC '06: Proceedings of the 2006 ACM symposium on Applied computing},
 year = {2006},
 isbn = {1-59593-108-2},
 pages = {1721--1727},
 location = {Dijon, France},
 doi = {http://doi.acm.org/10.1145/1141277.1141686},
 publisher = {ACM},
 address = {New York, NY, USA},
 }
 
 @inproceedings{ybp07-esec-fse,
 author = {Yu, F. and Bultan, T. and Peterson, E.},
 title = {Automated size analysis for OCL},
 booktitle = {ESEC-FSE '07: Proceedings of the the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The foundations of Software Engineering},
 year = {2007},
 isbn = {978-1-59593-811-4},
 pages = {331--340},
 location = {Dubrovnik, Croatia},
 doi = {http://doi.acm.org/10.1145/1287624.1287671},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@Article{ct07-scp,
author = {J. Cabot and E. Teniente},
title = {{Transformation techniques for OCL constraints}},
journal = {Science of Computer Programming},
year = {2007},
volume = {68},
number = {3},
pages = {179---195},
month = {October},
note = {Special Issue on Model Transformation},
}

@Manual{ocl,
title = {{UML 2.0 OCL Specification}},
author = {OMG},
year = {2003},
note = {OMG Adopted Specification (ptc/03-10-14)},
}
